even_number_of_swaps_of_identity: Identity permutations require an even number of transpositions
This theorem proves that if a list L of transpositions has product equal to the identity permutation,
then L.length must be even. The proof uses strong induction on the list length combined with a key
reduction lemma (exists_reduction) that produces two cases: either the list can be shortened by 2
while preserving the product (Case 1, handled by the induction hypothesis), or the product takes a specific
form that leads to a contradiction when the product is the identity (Case 2). The parity is therefore
preserved all the way down to the empty-list base case, where length 0 is trivially even.
Interactive Lean 4 proof ā click a line to see its strategy and explanation inline
Strategy: State the theorem ā a list of swaps whose product is the identity must have even length.
Explanation: The theorem takes three inputs: L, a list of permutations on a finite decidably-equal type Ī±; hL, the hypothesis that every element of L is a transposition (IsSwap); and hprod, the hypothesis that the product of all elements equals the identity. The type-class assumptions [DecidableEq Ī±] and [Fintype Ī±] are needed to work with Lean's permutation API and to talk about swaps concretely. The conclusion Even L.length asserts that the list has even length. This is the foundational result that makes the sign of a permutation well-defined.
Strategy: Name the list length so we can perform strong induction on it.
Explanation: We introduce a fresh natural number n and record the equality hn : L.length = n. This is necessary because Nat.strong_induction_on requires a standalone variable to induct on. Without this step, inducting directly on L.length would be syntactically awkward and would not allow us to generalize over different lists of the same length in the induction hypothesis.
Strategy: Strong induction on n ā the induction hypothesis covers all strictly smaller lengths.
Explanation: Strong induction gives ih : ā k < n, ā L', (ā Ļ ā L', Ļ.IsSwap) ā L'.prod = 1 ā L'.length = k ā Even k. We need strong (not simple) induction because the reduction lemma shortens the list by 2, not by 1 ā so we cannot just appeal to the immediate predecessor. The generalizing L keeps L universally quantified so the IH can be applied to different lists of the same smaller length.
Strategy: Substitute n back to L.length, cleaning up the context.
Explanation: Since hn : L.length = n, the subst tactic replaces every occurrence of n with L.length throughout the goal and hypotheses. This restores the goal to a direct statement about L and eliminates the auxiliary variable n, leaving a cleaner context for the structural induction that follows.
Strategy: Reverse induction on L ā split as nil or M ++ [s].
Explanation: List.reverseRecOn gives two cases: the empty list, and a list of the form M ++ [s] where s is the last element. We use reverse (right-to-left) induction rather than the standard front-cons induction because the reduction lemma exists_reduction is stated in terms of a prefix list M followed by a trailing swap ā exactly the shape M ++ [swap a b].
Strategy: Base case ā the empty list has length 0, which is even.
Explanation: When L = [], we need Even 0. The empty list's product is 1 by definition (the identity of the monoid), so hprod is trivially satisfied. Even 0 holds since 0 = 2 Ā· 0, and simp closes this immediately using the standard simp lemma for Even 0.
Strategy: Inductive case ā L = M ++ [s] where s is the last element.
Explanation: By reverse induction, L splits as M ++ [s]. The underscore discards the internal IH from List.reverseRecOn ā we will use the strong IH ih instead, which is strictly more powerful since it applies to any strictly shorter list, not just M.
Strategy: Extract that the last element s is a transposition.
Explanation: From hL : ā Ļ ā L, Ļ.IsSwap and the fact that s ā M ++ [s] (proved by simp), we derive hs : s.IsSwap. This is needed to destructure s into its two constituent elements in the next step.
Strategy: Destructure the swap ā extract elements a, b with a ā b and substitute s = swap a b.
Explanation: IsSwap s means ā a b, a ā b ā§ s = swap a b. The rcases destructs this, giving us a b : Ī±, hab : a ā b, and the rfl substitutes s with swap a b everywhere in the goal and context. From this point on, L is concretely M ++ [swap a b].
Strategy: Prove every element of the prefix M is also a swap.
Explanation: For any x ā M, we know x ā M ++ [swap a b] (proved by simp [hx]), so hL gives x.IsSwap. This hypothesis is required by exists_reduction, which needs to know that all elements of M are swaps before it can perform its reduction.
Strategy: Apply the key reduction lemma ā the combinatorial engine of the proof.
Explanation: exists_reduction M a b hab hM_swaps produces one of two outcomes. Left (Reduction): there exists a shorter list M' of swaps with M'.length + 2 = (M ++ [swap a b]).length and the same product ā the list can be shortened by 2 while preserving the product. Right (Move): there exists z ā a and a list M' of swaps such that (M ++ [swap a b]).prod = swap a z * M'.prod and every element of M' fixes a pointwise. These are the only two possibilities.
Strategy: Case 1 (Reduction) ā transfer the product-equals-identity hypothesis to M'.
Explanation: In the reduction case, h_equiv : M'.prod = (M ++ [swap a b]).prod. Since hprod : (M ++ [swap a b]).prod = 1, rewriting backwards with ā h_equiv gives hprod : M'.prod = 1. Now M' satisfies all the hypotheses needed to apply the strong induction hypothesis.
Strategy: Prove M' is strictly shorter than L ā the key condition for the strong IH.
Explanation: From hlen : M'.length + 2 = (M ++ [swap a b]).length, we need M'.length < (M ++ [swap a b]).length. After simp only unfolds the append and singleton lengths to arithmetic expressions, this becomes a simple linear arithmetic fact that omega closes immediately: if M'.length + 2 = k then M'.length < k.
Strategy: Instantiate the strong induction hypothesis at M' to get Even M'.length.
Explanation: We supply all required arguments to ih: the smaller length M'.length, the strict inequality h_lt, the list M' itself, the swap hypothesis hM'_swaps, the product hypothesis hprod (now rewritten to M'.prod = 1), and rfl for the trivial equality M'.length = M'.length. After specialization, ih : Even M'.length.
Strategy: Conclude Even L.length from Even M'.length and the length relation.
Explanation: The goal is Even (M ++ [swap a b]).length. After simp only this becomes Even (M.length + 1). Rewriting with ā hlen (which says M'.length + 2 = M.length + 1) transforms the goal to Even (M'.length + 2). Since Even M'.length holds (from the IH), and Even (k + 2) ā Even k for any k, grind closes this arithmetic parity argument automatically.
Strategy: Case 2 (Move) ā rewrite hprod using h_equiv to expose the contradiction.
Explanation: In the move case, h_equiv : (M ++ [swap a b]).prod = swap a z * M'.prod. Rewriting hprod with this gives hprod : swap a z * M'.prod = 1. This is the starting point for deriving a contradiction: if the product is identity, then applying both sides to a will force a = z, contradicting hza : z ā a.
Strategy: Apply both sides of the identity equation to the element a.
Explanation: Since hprod : swap a z * M'.prod = 1, rewriting gives h_apply : (1 : Perm Ī±) a = (swap a z * M'.prod) a. Applying a permutation equality pointwise to a specific element is the standard technique for extracting concrete information from an abstract permutation equation. The left side will simplify to a, and the right side will eventually simplify to z.
Strategy: Simplify the pointwise application ā reduce to a = swap a z (M'.prod a).
Explanation: Equiv.Perm.coe_one and id_eq simplify (1 : Perm Ī±) a to just a. Equiv.Perm.mul_apply expands (swap a z * M'.prod) a to swap a z (M'.prod a) (function composition, right-to-left). After simplification, h_apply : a = swap a z (M'.prod a).
Strategy: Prove M'.prod fixes a ā inline mini-lemma by structural induction on the list.
Explanation: We prove a helper: if every permutation in a list fixes a, then their product also fixes a. Base case (nil): the empty product is the identity, which fixes everything ā simp closes this. Inductive case (x :: xs): (x Ā· xs.prod)(a) = x(xs.prod(a)) by mul_apply; by the IH xs.prod(a) = a; then x(a) = a by hypothesis. We apply this helper to M' using hM'_fix, which says every element of M' fixes a (the second component .2 of the conjunction).
Strategy: Substitute the fixed point and evaluate the swap ā reducing h_apply to a = z.
Explanation: We have h_apply : a = swap a z (M'.prod a). Rewriting with h_fix (which says M'.prod a = a) gives a = swap a z a. Then swap_apply_left is the lemma swap a z a = z (a swap sends its left argument to its right argument). So after both rewrites, h_apply : a = z.
Strategy: Derive the final contradiction ā Case 2 is impossible.
Explanation: We have proven h_apply : a = z. But hza : z ā a!
h_apply.symm gives: z = ahza (z = a) produces: False (applying the inequality to the equality).elim: from False, prove anything (including the current goal)š” Tip: Click on any line above to see its strategy and explanation inline. Click again to hide it.
The proof follows a strong induction + contradiction argument:
Key insight: The "move" case is impossible when the product is identity, because moving a swap to the front would create swap(a,z) as a factor of the identity, but then applying both sides to 'a' reveals that z must equal a, contradicting the construction. So we always get reduction, which decreases length by 2, preserving parity until we reach the base case.
Uses Nat.strong_induction_on on the list length so the IH applies to
any strictly shorter list, not just the immediate predecessor. This is essential because
the reduction lemma shortens the list by 2, skipping over the predecessor entirely.
The key modular lemma that drives the proof. Given M and swap(a,b), it either produces a shorter equivalent list (Case 1) or rewrites the product as swap(a,z)Ā·M' where M' fixes a (Case 2). This clean case split is the combinatorial heart of the argument.
Case 2 is eliminated via contradiction: if the product is identity, the "move" form forces swap(a,z)Ā·M'.prod = 1. Applying to a and using the fixed-point property of M' yields a = z, contradicting z ā a.
Proves by structural induction that if every permutation in a list fixes a point, their product also fixes that point. Base case: identity fixes everything. Inductive case: compose the fixed-point properties step by step.
This theorem is fundamental in permutation group theory. It shows that the parity of a permutation (even vs. odd) is well-defined: you cannot write the identity using an odd number of transpositions. Combined with the other direction (any even-length list of swaps gives an even permutation), this establishes that the sign homomorphism sgn: Sā ā {Ā±1} is well-defined and that the alternating group Aā (even permutations) is indeed a proper subgroup of Sā of index 2. The proof technique ā strong induction with a reduction lemma producing a strict length decrease ā is a standard and reusable pattern for parity arguments in combinatorial formalisation in Lean 4.